\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$,$B$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$),\+
\\[0ex]$f$:(($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow$($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $g$:($\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}$), $L$,$L_{1}$,$l$:(event{-}info(${\it ds}$;${\it da}$) List).
\-\\[0ex]($L$ = append($L_{1}$; $l$))
\\[0ex]$\Rightarrow$ \=($\forall$${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List). \+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$)
\\[0ex]$\Rightarrow$ (iseg(event{-}info(${\it ds}$;${\it da}$); $L_{1}$; ${\it L'}$) $\Leftarrow\!\Rightarrow$ ($\uparrow$(ecl{-}trans{-}h($A$)(0,ecl{-}trans{-}state($A$; ${\it L'}$))))))
\-\\[0ex]$\Rightarrow$ (\=ecl{-}trans{-}state(combine{-}ecl{-}tuples($A$; $B$; $f$; $g$); $L$)\+
\\[0ex]=
\\[0ex]$<$ecl{-}trans{-}state($A$; $L$), ecl{-}trans{-}state($B$; $l$)$>$
\\[0ex]$\in$ ecl{-}trans{-}type(combine{-}ecl{-}tuples($A$; $B$; $f$; $g$)))
\-
\end{tabbing}